$\forall$$M_{1}$, $M_{2}$:MsgA. $M_{1}$ $\subseteq$ $M_{2}$ $\Rightarrow$ ($\forall$$a$:Id, $s$:$M_{2}$.state. $M_{2}$.pre($a$,$s$) $\Rightarrow$ $M_{1}$.pre($a$,$s$))